Based on the definition of the partial interpretation functions, we now prove the following substitution properties by mutual induction over raw terms and types.
Weakening, exchange, and contraction
Let be finite, and suppose is a function. Then:
For any raw type , the composite partial morphism is contained in the partial morphism .
For any raw term , the composite partial morphism is contained in the partial morphism .
For any raw term , the composite partial morphism is contained in the partial morphism .
Here and denote simultaneous capture-avoiding substitution of for each variable . When is a bijection, this asserts invariance under renaming of free variables. When is an inclusion, it asserts weakening, and when is surjective it is contraction. Note that in general these containments can be strict, e.g. if some variable in appears freely in or , then the composites may have empty domain while the morphisms they are being compared to might not.
Substitution
Let be finite and , while is a raw term. Then:
For any raw type , the composite partial morphism is contained in the partial morphism .
For any raw term , the composite partial morphism is contained in the partial morphism .
For any raw term , the composite partial morphism is contained in the partial morphism .
Inductive clauses
TODO.
Last revised on November 2, 2018 at 19:45:40.
See the history of this page for a list of all contributions to it.